<html xmlns:v="urn:schemas-microsoft-com:vml"
xmlns:o="urn:schemas-microsoft-com:office:office"
xmlns:w="urn:schemas-microsoft-com:office:word"
xmlns="http://www.w3.org/TR/REC-html40">

<head>
<meta http-equiv=Content-Type content="text/html; charset=iso-8859-1">
<meta name=ProgId content=Word.Document>
<meta name=Generator content="Microsoft Word 9">
<meta name=Originator content="Microsoft Word 9">
<link rel=File-List href="./AppendixF_files/filelist.xml">
<link rel=Edit-Time-Data href="./AppendixF_files/editdata.mso">
<!--[if !mso]>
<style>
v\:* {behavior:url(#default#VML);}
o\:* {behavior:url(#default#VML);}
w\:* {behavior:url(#default#VML);}
.shape {behavior:url(#default#VML);}
</style>
<![endif]-->
<title>Appendix F </title>
<style>
<!--
 /* Font Definitions */
@font-face
	{font-family:Tahoma;
	panose-1:2 11 6 4 3 5 4 4 2 4;
	mso-font-charset:0;
	mso-generic-font-family:swiss;
	mso-font-pitch:variable;
	mso-font-signature:1627421319 -2147483648 8 0 66047 0;}
@font-face
	{font-family:"Microsoft Sans Serif";
	panose-1:2 11 6 4 2 2 2 2 2 4;
	mso-font-charset:0;
	mso-generic-font-family:swiss;
	mso-font-pitch:variable;
	mso-font-signature:1627421663 -2147483648 8 0 66047 0;}
@font-face
	{font-family:BrushScrD;
	panose-1:3 0 0 0 0 0 0 0 0 0;
	mso-font-charset:0;
	mso-generic-font-family:script;
	mso-font-pitch:variable;
	mso-font-signature:-2147483473 30971 0 0 147 0;}
 /* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
	{mso-style-parent:"";
	margin:0in;
	margin-bottom:.0001pt;
	mso-pagination:widow-orphan;
	font-size:10.0pt;
	font-family:"Times New Roman";
	mso-fareast-font-family:"Times New Roman";
	color:windowtext;}
h1
	{mso-style-next:Normal;
	margin-top:0in;
	margin-right:-.35pt;
	margin-bottom:0in;
	margin-left:0in;
	margin-bottom:.0001pt;
	text-align:justify;
	mso-pagination:widow-orphan;
	page-break-after:avoid;
	mso-outline-level:1;
	font-size:11.0pt;
	mso-bidi-font-size:10.0pt;
	font-family:"Times New Roman";
	color:black;
	mso-font-kerning:0pt;
	mso-ansi-language:EN-GB;
	font-weight:normal;
	text-decoration:underline;
	text-underline:single;}
h2
	{mso-style-next:Normal;
	margin-top:0in;
	margin-right:-.35pt;
	margin-bottom:0in;
	margin-left:0in;
	margin-bottom:.0001pt;
	text-align:center;
	mso-pagination:widow-orphan;
	page-break-after:avoid;
	mso-outline-level:2;
	font-size:11.0pt;
	mso-bidi-font-size:10.0pt;
	font-family:"Times New Roman";
	color:black;
	mso-ansi-language:EN-GB;
	font-weight:normal;
	font-style:italic;
	mso-bidi-font-style:normal;}
h3
	{mso-style-next:Normal;
	margin-top:0in;
	margin-right:-.35pt;
	margin-bottom:0in;
	margin-left:0in;
	margin-bottom:.0001pt;
	text-align:justify;
	mso-pagination:widow-orphan;
	page-break-after:avoid;
	mso-outline-level:3;
	font-size:14.0pt;
	mso-bidi-font-size:10.0pt;
	font-family:"Times New Roman";
	color:black;
	mso-ansi-language:EN-GB;
	font-weight:normal;}
h4
	{mso-style-next:Normal;
	margin-top:0in;
	margin-right:-.35pt;
	margin-bottom:0in;
	margin-left:0in;
	margin-bottom:.0001pt;
	text-align:justify;
	mso-pagination:widow-orphan;
	page-break-after:avoid;
	mso-outline-level:4;
	font-size:11.0pt;
	mso-bidi-font-size:10.0pt;
	font-family:"Times New Roman";
	color:black;
	mso-ansi-language:EN-GB;
	font-weight:bold;
	mso-bidi-font-weight:normal;
	text-decoration:underline;
	text-underline:single;}
h5
	{mso-style-next:Normal;
	margin-top:0in;
	margin-right:-.35pt;
	margin-bottom:0in;
	margin-left:0in;
	margin-bottom:.0001pt;
	text-align:justify;
	mso-pagination:widow-orphan;
	page-break-after:avoid;
	mso-outline-level:5;
	font-size:14.0pt;
	mso-bidi-font-size:10.0pt;
	font-family:"Times New Roman";
	color:black;
	mso-ansi-language:EN-GB;
	font-weight:bold;
	mso-bidi-font-weight:normal;
	text-decoration:underline;
	text-underline:single;}
h6
	{mso-style-next:Normal;
	margin-top:0in;
	margin-right:-.35pt;
	margin-bottom:0in;
	margin-left:0in;
	margin-bottom:.0001pt;
	text-align:justify;
	text-indent:.5in;
	mso-pagination:widow-orphan;
	page-break-after:avoid;
	mso-outline-level:6;
	font-size:11.0pt;
	mso-bidi-font-size:10.0pt;
	font-family:"Times New Roman";
	color:black;
	mso-ansi-language:EN-GB;
	font-weight:normal;
	font-style:italic;
	mso-bidi-font-style:normal;}
p.MsoHeading7, li.MsoHeading7, div.MsoHeading7
	{mso-style-next:Normal;
	margin-top:0in;
	margin-right:-.35pt;
	margin-bottom:0in;
	margin-left:0in;
	margin-bottom:.0001pt;
	text-align:justify;
	mso-pagination:widow-orphan;
	page-break-after:avoid;
	mso-outline-level:7;
	font-size:11.0pt;
	mso-bidi-font-size:10.0pt;
	font-family:"Times New Roman";
	mso-fareast-font-family:"Times New Roman";
	color:black;
	mso-ansi-language:EN-GB;
	font-style:italic;
	mso-bidi-font-style:normal;}
p.MsoHeading8, li.MsoHeading8, div.MsoHeading8
	{mso-style-next:Normal;
	margin-top:0in;
	margin-right:-.35pt;
	margin-bottom:0in;
	margin-left:0in;
	margin-bottom:.0001pt;
	text-align:justify;
	mso-pagination:widow-orphan;
	page-break-after:avoid;
	mso-outline-level:8;
	font-size:14.0pt;
	mso-bidi-font-size:10.0pt;
	font-family:"Times New Roman";
	mso-fareast-font-family:"Times New Roman";
	color:black;
	mso-ansi-language:EN-GB;
	text-decoration:underline;
	text-underline:single;}
p.MsoHeading9, li.MsoHeading9, div.MsoHeading9
	{mso-style-next:Normal;
	margin-top:0in;
	margin-right:-.35pt;
	margin-bottom:0in;
	margin-left:0in;
	margin-bottom:.0001pt;
	text-align:center;
	mso-pagination:widow-orphan;
	page-break-after:avoid;
	mso-outline-level:9;
	font-size:11.0pt;
	mso-bidi-font-size:10.0pt;
	font-family:"Times New Roman";
	mso-fareast-font-family:"Times New Roman";
	color:black;
	mso-ansi-language:EN-GB;
	font-weight:bold;
	mso-bidi-font-weight:normal;}
p.MsoIndex1, li.MsoIndex1, div.MsoIndex1
	{mso-style-update:auto;
	mso-style-next:Normal;
	margin-top:0in;
	margin-right:0in;
	margin-bottom:0in;
	margin-left:11.0pt;
	margin-bottom:.0001pt;
	text-indent:-11.0pt;
	mso-pagination:widow-orphan;
	font-size:11.0pt;
	mso-bidi-font-size:10.5pt;
	font-family:"Times New Roman";
	mso-fareast-font-family:"Times New Roman";
	color:black;}
p.MsoIndex2, li.MsoIndex2, div.MsoIndex2
	{mso-style-update:auto;
	mso-style-next:Normal;
	margin-top:0in;
	margin-right:0in;
	margin-bottom:0in;
	margin-left:22.0pt;
	margin-bottom:.0001pt;
	text-indent:-11.0pt;
	mso-pagination:widow-orphan;
	font-size:11.0pt;
	mso-bidi-font-size:10.5pt;
	font-family:"Times New Roman";
	mso-fareast-font-family:"Times New Roman";
	color:black;}
p.MsoIndex3, li.MsoIndex3, div.MsoIndex3
	{mso-style-update:auto;
	mso-style-next:Normal;
	margin-top:0in;
	margin-right:0in;
	margin-bottom:0in;
	margin-left:33.0pt;
	margin-bottom:.0001pt;
	text-indent:-11.0pt;
	mso-pagination:widow-orphan;
	font-size:11.0pt;
	mso-bidi-font-size:10.5pt;
	font-family:"Times New Roman";
	mso-fareast-font-family:"Times New Roman";
	color:black;}
p.MsoIndex4, li.MsoIndex4, div.MsoIndex4
	{mso-style-update:auto;
	mso-style-next:Normal;
	margin-top:0in;
	margin-right:0in;
	margin-bottom:0in;
	margin-left:44.0pt;
	margin-bottom:.0001pt;
	text-indent:-11.0pt;
	mso-pagination:widow-orphan;
	font-size:11.0pt;
	mso-bidi-font-size:10.5pt;
	font-family:"Times New Roman";
	mso-fareast-font-family:"Times New Roman";
	color:black;}
p.MsoIndex5, li.MsoIndex5, div.MsoIndex5
	{mso-style-update:auto;
	mso-style-next:Normal;
	margin-top:0in;
	margin-right:0in;
	margin-bottom:0in;
	margin-left:55.0pt;
	margin-bottom:.0001pt;
	text-indent:-11.0pt;
	mso-pagination:widow-orphan;
	font-size:11.0pt;
	mso-bidi-font-size:10.5pt;
	font-family:"Times New Roman";
	mso-fareast-font-family:"Times New Roman";
	color:black;}
p.MsoIndex6, li.MsoIndex6, div.MsoIndex6
	{mso-style-update:auto;
	mso-style-next:Normal;
	margin-top:0in;
	margin-right:0in;
	margin-bottom:0in;
	margin-left:66.0pt;
	margin-bottom:.0001pt;
	text-indent:-11.0pt;
	mso-pagination:widow-orphan;
	font-size:11.0pt;
	mso-bidi-font-size:10.5pt;
	font-family:"Times New Roman";
	mso-fareast-font-family:"Times New Roman";
	color:black;}
p.MsoIndex7, li.MsoIndex7, div.MsoIndex7
	{mso-style-update:auto;
	mso-style-next:Normal;
	margin-top:0in;
	margin-right:0in;
	margin-bottom:0in;
	margin-left:77.0pt;
	margin-bottom:.0001pt;
	text-indent:-11.0pt;
	mso-pagination:widow-orphan;
	font-size:11.0pt;
	mso-bidi-font-size:10.5pt;
	font-family:"Times New Roman";
	mso-fareast-font-family:"Times New Roman";
	color:black;}
p.MsoIndex8, li.MsoIndex8, div.MsoIndex8
	{mso-style-update:auto;
	mso-style-next:Normal;
	margin-top:0in;
	margin-right:0in;
	margin-bottom:0in;
	margin-left:88.0pt;
	margin-bottom:.0001pt;
	text-indent:-11.0pt;
	mso-pagination:widow-orphan;
	font-size:11.0pt;
	mso-bidi-font-size:10.5pt;
	font-family:"Times New Roman";
	mso-fareast-font-family:"Times New Roman";
	color:black;}
p.MsoIndex9, li.MsoIndex9, div.MsoIndex9
	{mso-style-update:auto;
	mso-style-next:Normal;
	margin-top:0in;
	margin-right:0in;
	margin-bottom:0in;
	margin-left:99.0pt;
	margin-bottom:.0001pt;
	text-indent:-11.0pt;
	mso-pagination:widow-orphan;
	font-size:11.0pt;
	mso-bidi-font-size:10.5pt;
	font-family:"Times New Roman";
	mso-fareast-font-family:"Times New Roman";
	color:black;}
p.MsoFootnoteText, li.MsoFootnoteText, div.MsoFootnoteText
	{margin:0in;
	margin-bottom:.0001pt;
	mso-pagination:widow-orphan;
	font-size:11.0pt;
	mso-bidi-font-size:10.0pt;
	font-family:"Times New Roman";
	mso-fareast-font-family:"Times New Roman";
	color:black;}
p.MsoHeader, li.MsoHeader, div.MsoHeader
	{margin:0in;
	margin-bottom:.0001pt;
	mso-pagination:widow-orphan;
	tab-stops:center 207.65pt right 415.3pt;
	font-size:11.0pt;
	mso-bidi-font-size:10.0pt;
	font-family:"Times New Roman";
	mso-fareast-font-family:"Times New Roman";
	color:black;}
p.MsoFooter, li.MsoFooter, div.MsoFooter
	{margin:0in;
	margin-bottom:.0001pt;
	mso-pagination:widow-orphan;
	tab-stops:center 207.65pt right 415.3pt;
	font-size:11.0pt;
	mso-bidi-font-size:10.0pt;
	font-family:"Times New Roman";
	mso-fareast-font-family:"Times New Roman";
	color:black;}
p.MsoIndexHeading, li.MsoIndexHeading, div.MsoIndexHeading
	{mso-style-next:"Index 1";
	margin-top:12.0pt;
	margin-right:0in;
	margin-bottom:6.0pt;
	margin-left:0in;
	text-align:center;
	mso-pagination:widow-orphan;
	font-size:11.0pt;
	mso-bidi-font-size:15.5pt;
	font-family:"Times New Roman";
	mso-fareast-font-family:"Times New Roman";
	color:black;
	font-weight:bold;}
span.MsoFootnoteReference
	{vertical-align:super;}
span.MsoEndnoteReference
	{vertical-align:super;}
p.MsoEndnoteText, li.MsoEndnoteText, div.MsoEndnoteText
	{margin:0in;
	margin-bottom:.0001pt;
	mso-pagination:widow-orphan;
	font-size:10.0pt;
	font-family:"Times New Roman";
	mso-fareast-font-family:"Times New Roman";
	color:black;}
p.MsoTitle, li.MsoTitle, div.MsoTitle
	{margin:0in;
	margin-bottom:.0001pt;
	text-align:center;
	mso-pagination:widow-orphan;
	font-size:12.0pt;
	mso-bidi-font-size:10.0pt;
	font-family:"Times New Roman";
	mso-fareast-font-family:"Times New Roman";
	color:windowtext;
	font-weight:bold;
	mso-bidi-font-weight:normal;}
p.MsoBodyText, li.MsoBodyText, div.MsoBodyText
	{margin-top:0in;
	margin-right:-.35pt;
	margin-bottom:0in;
	margin-left:0in;
	margin-bottom:.0001pt;
	text-align:justify;
	mso-pagination:widow-orphan;
	font-size:11.0pt;
	mso-bidi-font-size:10.0pt;
	font-family:"Times New Roman";
	mso-fareast-font-family:"Times New Roman";
	color:black;
	mso-ansi-language:EN-GB;}
p.MsoBodyTextIndent, li.MsoBodyTextIndent, div.MsoBodyTextIndent
	{margin-top:0in;
	margin-right:0in;
	margin-bottom:0in;
	margin-left:13.5pt;
	margin-bottom:.0001pt;
	text-align:justify;
	text-indent:.65pt;
	mso-pagination:widow-orphan;
	mso-layout-grid-align:none;
	text-autospace:none;
	font-size:9.0pt;
	mso-bidi-font-size:10.0pt;
	font-family:"Times New Roman";
	mso-fareast-font-family:"Times New Roman";
	color:black;
	mso-ansi-language:EN-GB;}
p.MsoBodyText2, li.MsoBodyText2, div.MsoBodyText2
	{margin-top:0in;
	margin-right:-.35pt;
	margin-bottom:0in;
	margin-left:0in;
	margin-bottom:.0001pt;
	text-align:justify;
	mso-pagination:widow-orphan;
	border:none;
	mso-border-top-alt:solid windowtext 1.5pt;
	mso-border-bottom-alt:solid windowtext 1.5pt;
	padding:0in;
	mso-padding-alt:1.0pt 0in 1.0pt 0in;
	font-size:11.0pt;
	mso-bidi-font-size:10.0pt;
	font-family:"Times New Roman";
	mso-fareast-font-family:"Times New Roman";
	color:black;
	mso-ansi-language:EN-GB;}
p.MsoBodyText3, li.MsoBodyText3, div.MsoBodyText3
	{margin:0in;
	margin-bottom:.0001pt;
	text-align:justify;
	mso-pagination:widow-orphan;
	font-size:9.0pt;
	mso-bidi-font-size:10.0pt;
	font-family:"Times New Roman";
	mso-fareast-font-family:"Times New Roman";
	color:black;
	mso-ansi-language:EN-GB;}
p.MsoBodyTextIndent2, li.MsoBodyTextIndent2, div.MsoBodyTextIndent2
	{margin-top:0in;
	margin-right:0in;
	margin-bottom:0in;
	margin-left:13.5pt;
	margin-bottom:.0001pt;
	text-align:justify;
	mso-pagination:widow-orphan;
	mso-layout-grid-align:none;
	text-autospace:none;
	font-size:9.0pt;
	mso-bidi-font-size:10.0pt;
	font-family:"Times New Roman";
	mso-fareast-font-family:"Times New Roman";
	color:black;
	mso-ansi-language:EN-GB;}
p.MsoBodyTextIndent3, li.MsoBodyTextIndent3, div.MsoBodyTextIndent3
	{margin-top:0in;
	margin-right:0in;
	margin-bottom:0in;
	margin-left:.5in;
	margin-bottom:.0001pt;
	mso-pagination:widow-orphan;
	font-size:9.0pt;
	mso-bidi-font-size:10.0pt;
	font-family:"Times New Roman";
	mso-fareast-font-family:"Times New Roman";
	color:black;}
p.MsoBlockText, li.MsoBlockText, div.MsoBlockText
	{margin-top:0in;
	margin-right:-.35pt;
	margin-bottom:0in;
	margin-left:3.5in;
	margin-bottom:.0001pt;
	text-align:justify;
	text-indent:-3.5in;
	mso-pagination:widow-orphan;
	font-size:11.0pt;
	mso-bidi-font-size:10.0pt;
	font-family:"Times New Roman";
	mso-fareast-font-family:"Times New Roman";
	color:black;}
a:link, span.MsoHyperlink
	{mso-style-parent:"";
	color:blue;
	text-decoration:underline;
	text-underline:single;}
a:visited, span.MsoHyperlinkFollowed
	{color:purple;
	text-decoration:underline;
	text-underline:single;}
strong
	{mso-bidi-font-weight:normal;}
em
	{mso-bidi-font-style:normal;}
p.MsoDocumentMap, li.MsoDocumentMap, div.MsoDocumentMap
	{margin:0in;
	margin-bottom:.0001pt;
	mso-pagination:widow-orphan;
	background:navy;
	font-size:11.0pt;
	mso-bidi-font-size:10.0pt;
	font-family:Tahoma;
	mso-fareast-font-family:"Times New Roman";
	mso-bidi-font-family:"Times New Roman";
	color:black;}
p.MsoPlainText, li.MsoPlainText, div.MsoPlainText
	{margin:0in;
	margin-bottom:.0001pt;
	mso-pagination:widow-orphan;
	font-size:10.0pt;
	font-family:"Courier New";
	mso-fareast-font-family:"Times New Roman";
	mso-bidi-font-family:"Times New Roman";
	color:windowtext;
	mso-ansi-language:EN-GB;}
p
	{margin-right:0in;
	mso-margin-top-alt:auto;
	mso-margin-bottom-alt:auto;
	margin-left:0in;
	mso-pagination:widow-orphan;
	font-size:12.0pt;
	font-family:"Times New Roman";
	mso-fareast-font-family:"Times New Roman";
	color:black;}
span.Typewriter
	{mso-style-name:Typewriter;
	mso-style-parent:"";
	mso-ansi-font-size:10.0pt;
	mso-ascii-font-family:"Courier New";
	mso-hansi-font-family:"Courier New";}
span.l
	{mso-style-name:l;}
@page Section1
	{size:8.5in 11.0in;
	margin:1.0in 1.25in 1.0in 1.25in;
	mso-header-margin:.5in;
	mso-footer-margin:.5in;
	mso-paper-source:0;}
div.Section1
	{page:Section1;}
 /* List Definitions */
@list l0
	{mso-list-id:765854617;
	mso-list-type:hybrid;
	mso-list-template-ids:-1381705142 -749859354 67698713 67698715 67698703 67698713 67698715 67698703 67698713 67698715;}
@list l0:level1
	{mso-level-number-format:alpha-lower;
	mso-level-text:"\(%1\)";
	mso-level-tab-stop:.5in;
	mso-level-number-position:left;
	text-indent:-.25in;}
@list l1
	{mso-list-id:780999595;
	mso-list-type:hybrid;
	mso-list-template-ids:900252372 800498516 67698713 67698715 67698703 67698713 67698715 67698703 67698713 67698715;}
@list l1:level1
	{mso-level-number-format:alpha-upper;
	mso-level-tab-stop:.5in;
	mso-level-number-position:left;
	text-indent:-.25in;}
@list l2
	{mso-list-id:898514263;
	mso-list-type:hybrid;
	mso-list-template-ids:326562136 -475516452 67698713 67698715 67698703 67698713 67698715 67698703 67698713 67698715;}
@list l2:level1
	{mso-level-number-format:alpha-lower;
	mso-level-text:"\(%1\)";
	mso-level-tab-stop:.5in;
	mso-level-number-position:left;
	text-indent:-.25in;}
ol
	{margin-bottom:0in;}
ul
	{margin-bottom:0in;}
-->
</style>
<!--[if gte mso 9]><xml>
 <o:shapedefaults v:ext="edit" spidmax="1027"/>
</xml><![endif]--><!--[if gte mso 9]><xml>
 <o:shapelayout v:ext="edit">
  <o:idmap v:ext="edit" data="1"/>
 </o:shapelayout></xml><![endif]--><!--[if gte mso 9]><xml>
 <u1:DocumentProperties>
  <u1:Author> </u1:Author>
  <u1:Template>Normal</u1:Template>
  <u1:LastAuthor> </u1:LastAuthor>
  <u1:Revision>1</u1:Revision>
  <u1:TotalTime>0</u1:TotalTime>
  <u1:Created>2005-01-15T18:31:00Z</u1:Created>
  <u1:LastSaved>2005-01-15T18:31:00Z</u1:LastSaved>
  <u1:Pages>3</u1:Pages>
  <u1:Words>1715</u1:Words>
  <u1:Characters>9776</u1:Characters>
  <u1:Company> </u1:Company>
  <u1:Lines>81</u1:Lines>
  <u1:Paragraphs>19</u1:Paragraphs>
  <u1:CharactersWithSpaces>12005</u1:CharactersWithSpaces>
  <u1:Version>9.2720</u1:Version>
 </u1:DocumentProperties>
</xml><![endif]--><!--[if gte mso 9]><xml>
 <u2:WordDocument>
  <u2:DisplayHorizontalDrawingGridEvery>0</u2:DisplayHorizontalDrawingGridEvery>
  <u2:DisplayVerticalDrawingGridEvery>0</u2:DisplayVerticalDrawingGridEvery>
  <u2:UseMarginsForDrawingGridOrigin/>
  <u2:Compatibility>
   <u2:FootnoteLayoutLikeWW8/>
   <u2:ShapeLayoutLikeWW8/>
   <u2:AlignTablesRowByRow/>
   <u2:ForgetLastTabAlignment/>
   <u2:LayoutRawTableWidth/>
   <u2:LayoutTableRowsApart/>
  </u2:Compatibility>
 </u2:WordDocument>
</xml><![endif]-->
</head>

<body bgcolor=silver lang=EN-US link=blue vlink=purple style='tab-interval:
.5in'>

<div class=Section1>

<div align=center>

<table border=0 cellpadding=0 width="80%" bgcolor=white style='width:80.0%;
 mso-cellspacing:1.5pt;background:white;mso-padding-alt:75.0pt 75.0pt 75.0pt 75.0pt'>
 <tr>
  <td width="100%" style='width:100.0%;padding:75.0pt 75.0pt 75.0pt 75.0pt'>
  <p class=MsoTitle align=left style='margin-left:1.0in;text-align:left'><span
  style='font-size:14.0pt;mso-bidi-font-size:10.0pt;font-family:"Microsoft Sans Serif";
  font-weight:normal;mso-bidi-font-weight:bold'><![if !supportEmptyParas]>&nbsp;<![endif]><o:p></o:p></span></p>
  <div align=center>
  <table border=0 cellspacing=0 cellpadding=0 width=432 style='width:4.5in;
   border-collapse:collapse;border:none;mso-border-alt:solid windowtext .5pt;
   mso-padding-alt:0in 5.4pt 0in 5.4pt'>
   <tr>
    <td width=492 valign=top style='width:368.75pt;border:solid windowtext .5pt;
    padding:0in 5.4pt 0in 5.4pt'>
    <p class=MsoTitle align=left style='text-align:left'><span
    style='font-size:14.0pt;mso-bidi-font-size:10.0pt;font-family:"Microsoft Sans Serif";
    font-weight:normal;mso-bidi-font-weight:bold'><a href="QiPrograms.zip">Download
    Programs</a> <o:p></o:p></span></p>
    </td>
    <td width=492 valign=top style='width:368.75pt;border:solid windowtext .5pt;
    border-left:none;mso-border-left-alt:solid windowtext .5pt;padding:0in 5.4pt 0in 5.4pt'>
    <p class=MsoTitle align=left style='text-align:left'><span
    style='font-size:14.0pt;mso-bidi-font-size:10.0pt;font-family:"Microsoft Sans Serif";
    font-weight:normal;mso-bidi-font-weight:bold'><a href="contents.htm">Go to
    Contents Page</a><o:p></o:p></span></p>
    </td>
   </tr>
  </table>
  </div>
  <p class=MsoTitle align=left style='margin-left:1.0in;text-align:left'><span
  style='font-size:14.0pt;mso-bidi-font-size:10.0pt;font-family:"Microsoft Sans Serif";
  font-weight:normal;mso-bidi-font-weight:bold'><![if !supportEmptyParas]>&nbsp;<![endif]><o:p></o:p></span></p>
  <p class=MsoTitle align=left style='margin-left:1.0in;text-align:left'><span
  style='font-size:14.0pt;mso-bidi-font-size:10.0pt;font-family:"Microsoft Sans Serif";
  font-weight:normal;mso-bidi-font-weight:bold'>Note that this HTML page was
  generated from Word 2000.<span style="mso-spacerun: yes">&nbsp; </span>Some
  of the code cannot be pasted into Qi. You are advised to download the program
  files through the above link.<o:p></o:p></span></p>
  <p class=MsoNormal align=center style='margin-top:0in;margin-right:-.35pt;
  margin-bottom:0in;margin-left:.5in;margin-bottom:.0001pt;text-align:center;
  mso-outline-level:1'><span lang=EN-GB style='font-size:18.0pt;mso-bidi-font-size:
  10.0pt;font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman";
  mso-ansi-language:EN-GB'><![if !supportEmptyParas]>&nbsp;<![endif]><o:p></o:p></span></p>
  <p class=MsoNormal align=center style='margin-top:0in;margin-right:-.35pt;
  margin-bottom:0in;margin-left:.5in;margin-bottom:.0001pt;text-align:center;
  mso-outline-level:1'><span lang=EN-GB style='font-size:18.0pt;mso-bidi-font-size:
  10.0pt;font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman";
  mso-ansi-language:EN-GB'>Appendix F <u3:p></u3:p></span></p>
  <p class=MsoNormal align=center style='margin-top:0in;margin-right:-.35pt;
  margin-bottom:0in;margin-left:.5in;margin-bottom:.0001pt;text-align:center'><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal align=center style='margin-left:.5in;text-align:center'><span
  style='font-size:18.0pt;mso-bidi-font-size:10.0pt;font-family:BrushScrD;
  mso-bidi-font-style:italic'>T</span><span style='font-size:18.0pt;mso-bidi-font-size:
  10.0pt;font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>
  and the </span><span style='font-size:18.0pt;mso-bidi-font-size:10.0pt;
  font-family:BrushScrD;mso-bidi-font-style:italic'>L</span><span
  style='font-size:18.0pt;mso-bidi-font-size:10.0pt;font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-bidi-font-style:italic'> </span><span
  style='font-size:18.0pt;mso-bidi-font-size:10.0pt;font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>Type System<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><b><u><span
  style='font-size:14.0pt;mso-bidi-font-size:10.0pt;font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>The AB
  Theorem__________________________<u3:p></u3:p></span></u></b></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><b><u><span
  style='font-size:14.0pt;mso-bidi-font-size:10.0pt;font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>&nbsp;<u3:p></u3:p></span></u></b></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>One desirable property of a type
  checking procedure is that it is terminating, sound and complete; that is to
  say, the procedure constitutes a decision procedure for the type system in
  question.<span style="mso-spacerun: yes">&nbsp; </span>Fairly obviously, </span><span
  lang=EN-GB style='font-family:BrushScrD;mso-ansi-language:EN-GB;mso-bidi-font-style:
  italic'>T</span><span lang=EN-GB style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-ansi-language:EN-GB'> is sound
  (since it uses only the type rules for </span><span lang=EN-GB
  style='font-family:BrushScrD;mso-ansi-language:EN-GB;mso-bidi-font-style:
  italic'>L</span><span lang=EN-GB style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-ansi-language:EN-GB'>).<span
  style="mso-spacerun: yes">&nbsp; </span>Moreover the previous appendix
  established the type security of the system itself.<span style="mso-spacerun:
  yes">&nbsp; </span>We will prove </span><span lang=EN-GB style='font-family:
  BrushScrD;mso-ansi-language:EN-GB;mso-bidi-font-style:italic'>T</span><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'> is terminating.<span
  style="mso-spacerun: yes">&nbsp; </span>We shall see later </span><span
  lang=EN-GB style='font-family:BrushScrD;mso-ansi-language:EN-GB;mso-bidi-font-style:
  italic'>T</span><span lang=EN-GB style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-ansi-language:EN-GB'> is
  incomplete in respect of the type rules for </span><span lang=EN-GB
  style='font-family:BrushScrD;mso-ansi-language:EN-GB;mso-bidi-font-style:
  italic'>L</span><span lang=EN-GB style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-ansi-language:EN-GB'>, but can be
  made complete to a subset of</span><span lang=EN-GB style='font-family:BrushScrD;
  mso-ansi-language:EN-GB;mso-bidi-font-style:italic'> L</span><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>.<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>We first have to prove a theorem
  based on the nature of the type rules that </span><span lang=EN-GB
  style='font-family:BrushScrD;mso-ansi-language:EN-GB;mso-bidi-font-style:
  italic'>T</span><span lang=EN-GB style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-ansi-language:EN-GB'> uses.<span
  style="mso-spacerun: yes">&nbsp; </span>The type rules are of two kinds.<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:1.0in;text-align:justify;text-indent:
  -.25in;mso-list:l1 level1 lfo2;tab-stops:list .5in'><![if !supportLists]>A.<span
  style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span><![endif]><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>A.</span><span lang=EN-GB
  style='font-size:7.0pt;mso-ansi-language:EN-GB'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
  </span><span lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>Type rules that eliminate goals
  without producing subgoals.<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:1.0in;text-align:justify;text-indent:
  -.25in;mso-list:l1 level1 lfo2;tab-stops:list .5in'><![if !supportLists]>B.<span
  style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; </span><![endif]><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>B.</span><span lang=EN-GB
  style='font-size:7.0pt;mso-ansi-language:EN-GB'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
  </span><span lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>Type rules that generate subgoals
  but reduce the bracketing of an expression in the original goal.<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify;mso-layout-grid-align:
  none;text-autospace:none'><span lang=EN-GB style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-ansi-language:EN-GB'>We will call
  these &#8216;A-rules&#8217; and &#8216;B-rules&#8217; respectively.<span style="mso-spacerun:
  yes">&nbsp; </span>Let us say that a sequent system is an <b>AB system</b> if
  every rule in it is an A-rule or a B-rule. Intuitively, any proof procedure
  which uses an AB system by applying all the rules in it will eventually
  generate a fixpoint.<span style="mso-spacerun: yes">&nbsp; </span>In other
  words, it needs to be proved that there is no infinite chain of rule
  applications R<sub>1</sub>, R<sub>2</sub>, R<sub>3</sub>, &#8230;. which can be
  successively applied to a series of goals G such that for all n, R<sub>n</sub>(&#8230;(R<sub>1</sub>(G)))
  </span><span style='mso-bidi-font-size:12.0pt;font-family:Symbol'>�</span><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'> R<sub>n+1</sub>(&#8230;(R<sub>n</sub>
  (R<sub>1</sub>(G)))).<span style="mso-spacerun: yes">&nbsp; </span>The
  theorem that states this is the <b>AB theorem</b></span><!--[if supportFields]><b><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'><span style='mso-element:field-begin'></span></span></b><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>
  XE &quot;<span style='mso-bidi-font-weight:bold'>AB theorem</span>&quot; </span><![endif]--><!--[if supportFields]><b><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'><span style='mso-element:field-end'></span></span></b><![endif]--><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>. <span style="mso-spacerun:
  yes">&nbsp;</span><u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>To prove this formally, we need a
  function, </span><span lang=EN-GB style='font-family:Symbol;mso-ansi-language:
  EN-GB'>b</span><span lang=EN-GB style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-ansi-language:EN-GB'>, which
  returns a value based on the bracketing found in the expressions used in the
  proof procedure.<span style="mso-spacerun: yes">&nbsp; </span>We begin by
  inductively defining </span><span lang=EN-GB style='font-family:Symbol;
  mso-ansi-language:EN-GB'>b</span><span lang=EN-GB style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-ansi-language:EN-GB'> for
  typings.<span style="mso-spacerun: yes">&nbsp; </span>A typing is an
  expression of the form <i>x</i> </span><span lang=EN-GB style='font-family:
  Symbol;mso-ansi-language:EN-GB'>: t</span><span lang=EN-GB style='font-family:
  "Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman";mso-ansi-language:
  EN-GB'>, where <i>x</i> is an expression of </span><span lang=EN-GB
  style='font-family:BrushScrD;mso-ansi-language:EN-GB;mso-bidi-font-style:
  italic'>L</span><span lang=EN-GB style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-ansi-language:EN-GB'> and </span><span
  lang=EN-GB style='font-family:Symbol;mso-ansi-language:EN-GB'>t</span><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'> is a type expression.<span
  style="mso-spacerun: yes">&nbsp; </span>Typings are effectively the
  well-formed formulae of a proof conducted by </span><span lang=EN-GB
  style='font-family:BrushScrD;mso-ansi-language:EN-GB;mso-bidi-font-style:
  italic'>T</span><span lang=EN-GB style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-ansi-language:EN-GB'>.<span
  style="mso-spacerun: yes">&nbsp; </span>Type expressions are defined
  inductively.<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>A symbol is a type expression.<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>If <i>a</i> is a type expression
  and <i>b</i> is a type expression and <i>v</i> is a variable, then (<i>a</i> </span><span
  style='font-family:Symbol'>�</span><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-ansi-language:EN-GB'> <i><span
  lang=EN-GB>b</span></i><span lang=EN-GB>), (<i>a</i> * <i>b</i>),<span
  style="mso-spacerun: yes">&nbsp; </span>(list <i>a</i>), (</span></span><span
  lang=EN-GB style='font-family:Symbol;mso-ansi-language:EN-GB'>&quot;</span><i><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>v a</span></i><span lang=EN-GB
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman";
  mso-ansi-language:EN-GB'>) are type expressions.<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>The function </span><span
  lang=EN-GB style='font-family:Symbol;mso-ansi-language:EN-GB'>b</span><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'> is defined inductively over
  typings as follows.<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:Symbol;mso-ansi-language:EN-GB'>b</span><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>(x : t) = </span><span lang=EN-GB
  style='font-family:Symbol;mso-ansi-language:EN-GB'>b</span><span lang=EN-GB
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman";
  mso-ansi-language:EN-GB'>(x) + 1<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>For </span><span lang=EN-GB
  style='font-family:BrushScrD;mso-ansi-language:EN-GB;mso-bidi-font-style:
  italic'>L</span><span lang=EN-GB style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-ansi-language:EN-GB'> expressions,
  </span><span lang=EN-GB style='font-family:Symbol;mso-ansi-language:EN-GB'>b</span><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'> is defined as follows.<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:Symbol;mso-ansi-language:EN-GB'>b</span><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>(x) = 0 if x is a primitive object<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:Symbol;mso-ansi-language:EN-GB'>b</span><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>(x<sub>1</sub> &#8230;.x<sub>n</sub>) = </span><span
  lang=EN-GB style='font-family:Symbol;mso-font-kerning:1.0pt;mso-ansi-language:
  EN-GB'>S</span><span lang=EN-GB style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-ansi-language:EN-GB'>(x<sub>i</sub>)
  + 1 for i =1 to i = n.<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>If </span><span lang=EN-GB
  style='font-family:Symbol;mso-ansi-language:EN-GB'>b</span><span lang=EN-GB
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman";
  mso-ansi-language:EN-GB'>(<i>x</i>) = <i>n</i> we say that the <b>B-value</b>
  of <i>x</i> is <i>n</i>. Given a sequent </span><span lang=EN-GB
  style='font-family:Symbol;mso-font-kerning:1.0pt;mso-ansi-language:EN-GB'>D</span><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'> &gt;&gt; C, we associate it to
  the B-value of this sequent by the following equation.<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:Symbol;mso-ansi-language:EN-GB'>b</span><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>(</span><span lang=EN-GB
  style='font-family:Symbol;mso-font-kerning:1.0pt;mso-ansi-language:EN-GB'>D</span><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'> &gt;&gt; C) = </span><span
  lang=EN-GB style='font-family:Symbol;mso-font-kerning:1.0pt;mso-ansi-language:
  EN-GB'>S</span><span lang=EN-GB style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-ansi-language:EN-GB'>(</span><span
  lang=EN-GB style='font-family:Symbol;mso-font-kerning:1.0pt;mso-ansi-language:
  EN-GB'>b</span><span lang=EN-GB style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-ansi-language:EN-GB'>(x<sub>i</sub>))
  + </span><span lang=EN-GB style='font-family:Symbol;mso-ansi-language:EN-GB'>b</span><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>(C) for all x<sub>i</sub> in </span><span
  lang=EN-GB style='font-family:Symbol;mso-font-kerning:1.0pt;mso-ansi-language:
  EN-GB'>D</span><span lang=EN-GB style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-ansi-language:EN-GB'>.<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>In other words to calculate the
  B-value of a sequent we simply total the B-values of its constituent
  wffs.<span style="mso-spacerun: yes">&nbsp;&nbsp; </span>We can now define a
  B-rule precisely.<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;mso-layout-grid-align:none;
  text-autospace:none'><span lang=EN-GB style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-ansi-language:EN-GB'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;mso-layout-grid-align:none;
  text-autospace:none'><span lang=EN-GB style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-ansi-language:EN-GB'>A rule R is a
  B-rule just if whenever R is successfully applied to a tuple of goals &lt;G<sub>0</sub>,
  G<sub>1</sub>,&#8230;, G<sub>n</sub>&gt;, the resulting tuple of goals &lt;G*<sub>1</sub>,&#8230;,G*<sub>m</sub>,
  G<sub>1</sub>, &#8230;, G<sub>n</sub>&gt;<span style="mso-spacerun: yes">&nbsp;
  </span>is such that </span><span lang=EN-GB style='font-family:Symbol;
  mso-ansi-language:EN-GB'>b</span><span lang=EN-GB style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-ansi-language:EN-GB'>(G*<sub>i</sub>)<span
  style="mso-spacerun: yes">&nbsp; </span>&lt; </span><span lang=EN-GB
  style='font-family:Symbol;mso-ansi-language:EN-GB'>b</span><span lang=EN-GB
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman";
  mso-ansi-language:EN-GB'>(G<sub>0</sub>) for all i, where 1 </span><span
  style='font-size:12.0pt;font-family:Symbol'>� </span><span lang=EN-GB
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman";
  mso-ansi-language:EN-GB'><span style="mso-spacerun: yes">&nbsp;</span>i </span><span
  style='font-size:12.0pt;font-family:Symbol'>� </span><span lang=EN-GB
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman";
  mso-ansi-language:EN-GB'><span style="mso-spacerun: yes">&nbsp;</span>m.<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><b><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>Theorem:</span></b><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'><span style="mso-spacerun:
  yes">&nbsp; </span>all the rules of the type system for </span><span
  lang=EN-GB style='font-family:BrushScrD;mso-ansi-language:EN-GB;mso-bidi-font-style:
  italic'>L</span><span lang=EN-GB style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-ansi-language:EN-GB'> are B-type
  rules with the exception of the Primitive, Sequents, Generalisation and
  Specialisation Rules.<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><b><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>Proof:</span></b><span lang=EN-GB
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman";
  mso-ansi-language:EN-GB'><span style="mso-spacerun: yes">&nbsp; </span>the
  proof is long but straightforward.<span style="mso-spacerun: yes">&nbsp;
  </span>We will cover one case and leave it to the reader to complete the
  other cases.<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>The Conditional Rule states<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><u><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>X : boolean; Y : A;<span
  style="mso-spacerun: yes">&nbsp; </span>Z : A;<u3:p></u3:p></span></u></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>(if X Y Z) : A;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>Let &lt;G<sub>0</sub>, G<sub>1</sub>,
  &#8230;, .G<sub>n</sub>&gt; be a tuple of goals.<span style="mso-spacerun:
  yes">&nbsp; </span>Assume </span><span lang=EN-GB style='font-family:Symbol;
  mso-ansi-language:EN-GB'>b</span><span lang=EN-GB style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-ansi-language:EN-GB'>(G<sub>0</sub>)
  = <i>m</i><span style="mso-spacerun: yes">&nbsp; </span>Assume the
  Conditional Rule is successfully applied to &lt;G<sub>0</sub>, G<sub>1</sub>,
  &#8230;, .G<sub>n</sub>&gt;.<span style="mso-spacerun: yes">&nbsp; </span>If so,
  then G<sub>0</sub> is of the form </span><span lang=EN-GB style='font-family:
  Symbol;mso-font-kerning:1.0pt;mso-ansi-language:EN-GB'>D</span><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'> &gt;&gt; (if X Y Z) : A, and the
  output of the rule application is &lt;G<sub>x</sub>, G<sub>y</sub>, G<sub>z</sub>,
  G<sub>1</sub>, &#8230;, .G<sub>n</sub>&gt; where G<sub>x</sub>, G<sub>y</sub>, and
  G<sub>z</sub> are defined as follows. <span style="mso-spacerun:
  yes">&nbsp;</span><u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>G<sub>x</sub> = </span><span
  lang=EN-GB style='font-family:Symbol;mso-font-kerning:1.0pt;mso-ansi-language:
  EN-GB'>D</span><span lang=EN-GB style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-ansi-language:EN-GB'> &gt;&gt; X :
  boolean<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>G<sub>y</sub> = </span><span
  lang=EN-GB style='font-family:Symbol;mso-font-kerning:1.0pt;mso-ansi-language:
  EN-GB'>D</span><span lang=EN-GB style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-ansi-language:EN-GB'> &gt;&gt; Y :
  A<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>G<sub>z</sub> = </span><span
  lang=EN-GB style='font-family:Symbol;mso-font-kerning:1.0pt;mso-ansi-language:
  EN-GB'>D</span><span lang=EN-GB style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-ansi-language:EN-GB'> &gt;&gt; Z :
  A<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>We have the following equalities<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman";
  mso-ansi-language:EN-GB'><span style="mso-spacerun: yes">&nbsp;</span></span><span
  lang=EN-GB style='font-family:Symbol;mso-ansi-language:EN-GB'>b</span><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>(G<sub>0</sub>) = <i>m = </i></span><span
  lang=EN-GB style='font-family:Symbol;mso-ansi-language:EN-GB'>b</span><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>(</span><span lang=EN-GB
  style='font-family:Symbol;mso-font-kerning:1.0pt;mso-ansi-language:EN-GB'>D</span><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>) + </span><span lang=EN-GB
  style='font-family:Symbol;mso-ansi-language:EN-GB'>b</span><span lang=EN-GB
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman";
  mso-ansi-language:EN-GB'>((if X Y Z) : A)<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:Symbol;mso-ansi-language:EN-GB'><span
  style="mso-spacerun: yes">&nbsp;</span>b</span><span lang=EN-GB
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman";
  mso-ansi-language:EN-GB'>(G<sub>x</sub>) = </span><span lang=EN-GB
  style='font-family:Symbol;mso-ansi-language:EN-GB'>b</span><span lang=EN-GB
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman";
  mso-ansi-language:EN-GB'>(</span><span lang=EN-GB style='font-family:Symbol;
  mso-font-kerning:1.0pt;mso-ansi-language:EN-GB'>D</span><span lang=EN-GB
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman";
  mso-ansi-language:EN-GB'>) + </span><span lang=EN-GB style='font-family:Symbol;
  mso-ansi-language:EN-GB'>b</span><span lang=EN-GB style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-ansi-language:EN-GB'>(X : boolean)<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:Symbol;mso-ansi-language:EN-GB'><span
  style="mso-spacerun: yes">&nbsp;</span>b</span><span lang=EN-GB
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman";
  mso-ansi-language:EN-GB'>(G<sub>y</sub>) = </span><span lang=EN-GB
  style='font-family:Symbol;mso-ansi-language:EN-GB'>b</span><span lang=EN-GB
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman";
  mso-ansi-language:EN-GB'>(</span><span lang=EN-GB style='font-family:Symbol;
  mso-font-kerning:1.0pt;mso-ansi-language:EN-GB'>D</span><span lang=EN-GB
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman";
  mso-ansi-language:EN-GB'>) + </span><span lang=EN-GB style='font-family:Symbol;
  mso-ansi-language:EN-GB'>b</span><span lang=EN-GB style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-ansi-language:EN-GB'>(Y : A)<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:Symbol;mso-ansi-language:EN-GB'><span
  style="mso-spacerun: yes">&nbsp;</span>b</span><span lang=EN-GB
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman";
  mso-ansi-language:EN-GB'>(G<sub>z</sub>) = </span><span lang=EN-GB
  style='font-family:Symbol;mso-ansi-language:EN-GB'>b</span><span lang=EN-GB
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman";
  mso-ansi-language:EN-GB'>(</span><span lang=EN-GB style='font-family:Symbol;
  mso-font-kerning:1.0pt;mso-ansi-language:EN-GB'>D</span><span lang=EN-GB
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman";
  mso-ansi-language:EN-GB'>) + </span><span lang=EN-GB style='font-family:Symbol;
  mso-ansi-language:EN-GB'>b</span><span lang=EN-GB style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-ansi-language:EN-GB'>(Z : A)<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>But by the definition of </span><span
  lang=EN-GB style='font-family:Symbol;mso-ansi-language:EN-GB'>b</span><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>, the following inequalities hold.<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:Symbol;mso-ansi-language:EN-GB'>b</span><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>(X : boolean) &lt; </span><span
  lang=EN-GB style='font-family:Symbol;mso-ansi-language:EN-GB'>b</span><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>((if X Y Z) : A)<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:Symbol;mso-ansi-language:EN-GB'>b</span><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>(Y : A) &lt;<span
  style="mso-spacerun: yes">&nbsp; </span></span><span lang=EN-GB
  style='font-family:Symbol;mso-ansi-language:EN-GB'>b</span><span lang=EN-GB
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman";
  mso-ansi-language:EN-GB'>((if X Y Z) : A) <span style="mso-spacerun:
  yes">&nbsp;</span><u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:Symbol;mso-ansi-language:EN-GB'>b</span><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>(Z : A) &lt;<span
  style="mso-spacerun: yes">&nbsp; </span></span><span lang=EN-GB
  style='font-family:Symbol;mso-ansi-language:EN-GB'>b</span><span lang=EN-GB
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman";
  mso-ansi-language:EN-GB'>((if X Y Z) : A)<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>Abbreviating </span><span
  lang=EN-GB style='font-family:Symbol;mso-ansi-language:EN-GB'>b</span><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>(</span><span lang=EN-GB
  style='font-family:Symbol;mso-font-kerning:1.0pt;mso-ansi-language:EN-GB'>D</span><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>) by <i>d</i> and </span><span
  lang=EN-GB style='font-family:Symbol;mso-ansi-language:EN-GB'>b</span><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>((if X Y Z) : A) by <i>i</i>, and </span><span
  lang=EN-GB style='font-family:Symbol;mso-ansi-language:EN-GB'>b</span><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>(X : boolean), </span><span
  lang=EN-GB style='font-family:Symbol;mso-ansi-language:EN-GB'>b</span><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>(Y : A) and </span><span
  lang=EN-GB style='font-family:Symbol;mso-ansi-language:EN-GB'>b</span><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>(Z : A) by <i>x</i>, <i>y</i> and <i>z</i>
  respectively, we have the following equalities.<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:Symbol;mso-ansi-language:EN-GB'>b</span><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>(G<sub>0</sub>) = <i>m</i> = <i>d</i>
  + <i>i</i><u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:Symbol;mso-ansi-language:EN-GB'>b</span><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>(G<sub>x</sub>) = <i>d</i> + <i>x</i>
  where <i>x</i> &lt; <i>i</i><u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:Symbol;mso-ansi-language:EN-GB'>b</span><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>(G<sub>y</sub>) = <i>d</i> + <i>y</i>
  where y &lt; <i>i</i><u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:Symbol;mso-ansi-language:EN-GB'>b</span><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>(G<sub>z</sub>) = <i>d</i> + <i>z</i>
  where z &lt; <i>i</i><u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>Hence </span><span lang=EN-GB
  style='font-family:Symbol;mso-ansi-language:EN-GB'>b</span><span lang=EN-GB
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman";
  mso-ansi-language:EN-GB'>(G<sub>x</sub>) &lt; </span><span lang=EN-GB
  style='font-family:Symbol;mso-ansi-language:EN-GB'>b</span><span lang=EN-GB
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman";
  mso-ansi-language:EN-GB'>(G<sub>0</sub>) and </span><span lang=EN-GB
  style='font-family:Symbol;mso-ansi-language:EN-GB'>b</span><span lang=EN-GB
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman";
  mso-ansi-language:EN-GB'>(G<sub>y</sub>) &lt; </span><span lang=EN-GB
  style='font-family:Symbol;mso-ansi-language:EN-GB'>b</span><span lang=EN-GB
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman";
  mso-ansi-language:EN-GB'>(G<sub>0</sub>) and </span><span lang=EN-GB
  style='font-family:Symbol;mso-ansi-language:EN-GB'>b</span><span lang=EN-GB
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman";
  mso-ansi-language:EN-GB'>(G<sub>z</sub>) &lt; </span><span lang=EN-GB
  style='font-family:Symbol;mso-ansi-language:EN-GB'>b</span><span lang=EN-GB
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman";
  mso-ansi-language:EN-GB'>(G<sub>0</sub>) and the Conditional Rule is a B-rule.<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><b><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>&nbsp;<u3:p></u3:p></span></b></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><b><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>Theorem:</span></b><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'><span style="mso-spacerun:
  yes">&nbsp; </span>the Primitive and Sequents Rules are A-rules.<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><b><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>Proof:</span></b><span lang=EN-GB
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman";
  mso-ansi-language:EN-GB'> by inspection of the rules.<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><b><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>Corollary:</span></b><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'> the type system for </span><span
  lang=EN-GB style='font-family:BrushScrD;mso-ansi-language:EN-GB;mso-bidi-font-style:
  italic'>L</span><span lang=EN-GB style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-ansi-language:EN-GB'>, excepting
  the Specialisation Rule, is an AB system.<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>The omission of the <i>Specialisation
  Rule</i> is generally not important in </span><span lang=EN-GB
  style='font-family:BrushScrD;mso-ansi-language:EN-GB;mso-bidi-font-style:
  italic'>T</span><span lang=EN-GB style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-ansi-language:EN-GB'>, since unification
  is used to bind variables.<span style="mso-spacerun: yes">&nbsp;&nbsp;
  </span>The omission of this rule and the <i>Generalisation Rule</i> will be
  discussed later.<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>An <b>AB series</b> is a series of
  lists of goals where (a) the first list contains a single goal (b) for any
  element G<sub>n</sub> in the series, the immediate successor G<sub>n+1</sub>
  is generated from G<sub>n</sub> by the successful application of an A-rule or
  a B-rule.<span style="mso-spacerun: yes">&nbsp;&nbsp; </span>To prove the
  termination of </span><span lang=EN-GB style='font-family:BrushScrD;
  mso-ansi-language:EN-GB;mso-bidi-font-style:italic'>T</span><span lang=EN-GB
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman";
  mso-ansi-language:EN-GB'>, we have to prove that there is no infinite AB
  series.<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>Since the </span><span lang=EN-GB
  style='font-family:Symbol;mso-ansi-language:EN-GB'>b</span><span lang=EN-GB
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman";
  mso-ansi-language:EN-GB'> function maps every sequent to its B-value, we can
  associate each element in an AB series with a list of numbers.<span
  style="mso-spacerun: yes">&nbsp; </span>Each number is the B-value of the
  sequent in the goal.<span style="mso-spacerun: yes">&nbsp;&nbsp;
  </span>Therefore we extend the concept of a B-value (and hence the domain of </span><span
  lang=EN-GB style='font-family:Symbol;mso-ansi-language:EN-GB'>b</span><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>) to embrace goals and AB series.<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>Let G be a goal, where G = [s<sub>1</sub>,&#8230;,s<sub>m</sub>]
  and let </span><span lang=EN-GB style='font-family:Symbol;mso-ansi-language:
  EN-GB'>b</span><span lang=EN-GB style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-ansi-language:EN-GB'>(s<sub>1</sub>)
  = n<sub>1</sub>,&#8230;.,</span><span lang=EN-GB style='font-family:Symbol;
  mso-ansi-language:EN-GB'>b</span><span lang=EN-GB style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-ansi-language:EN-GB'>(s<sub>m</sub>)
  = n<sub>m</sub>.<span style="mso-spacerun: yes">&nbsp; </span>The B-value of
  the goal G is the list of numbers [n<sub>1</sub>,&#8230;,n<sub>m</sub>].<span
  style="mso-spacerun: yes">&nbsp;&nbsp; </span>Let G<sub>0</sub>, &#8230;.,G<sub>n</sub>
  be any series of goals.<span style="mso-spacerun: yes">&nbsp;&nbsp;
  </span>The B-value of this series is just the series </span><span lang=EN-GB
  style='font-family:Symbol;mso-ansi-language:EN-GB'>b</span><span lang=EN-GB
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman";
  mso-ansi-language:EN-GB'>(G<sub>0</sub>),&#8230;,</span><span lang=EN-GB
  style='font-family:Symbol;mso-ansi-language:EN-GB'>b</span><span lang=EN-GB
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman";
  mso-ansi-language:EN-GB'>(G<sub>n</sub>).<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>The B-value of an AB series is
  therefore a numeric representation of that series; it consists of a series of
  lists of numbers.<span style="mso-spacerun: yes">&nbsp;&nbsp; </span>Let us
  call such a series, an <b>ABn series</b>. Since this series is derived by a
  mapping from an AB series, it has the following property.<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>Let L<sub>n</sub> and L<sub>n+1</sub>
  be elements of an ABn series and let <i>a</i> be the number at the head of L<sub>n</sub>.<span
  style="mso-spacerun: yes">&nbsp; </span>Then either <u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:1.0in;text-align:justify;text-indent:
  -.25in;mso-list:l2 level1 lfo4;tab-stops:list .5in'><![if !supportLists]>(a)<span
  style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp; </span><![endif]><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>(a)</span><span lang=EN-GB
  style='font-size:7.0pt;mso-ansi-language:EN-GB'>&nbsp;&nbsp;&nbsp; </span><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>L<sub>n+1</sub> is the tail of L<sub>n</sub>
  (L<sub>n+1</sub> = tail(L<sub>n</sub>)) or <u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:1.0in;text-align:justify;text-indent:
  -.25in;mso-list:l2 level1 lfo4;tab-stops:list .5in'><![if !supportLists]>(b)<span
  style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp; </span><![endif]><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>(b)</span><span lang=EN-GB
  style='font-size:7.0pt;mso-ansi-language:EN-GB'>&nbsp;&nbsp;&nbsp; </span><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>L<sub>n+1</sub> is identical to
  the result of appending a list [<i>b</i><sub>1</sub>,&#8230;,<i>b</i><sub>k</sub>]
  to tail(L<sub>n</sub>) such that for each <i>b</i><sub>i</sub>, <i>b</i><sub>i</sub>
  &lt; <i>a</i>.<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>In the case (a), the inverse of L<sub>n+1</sub>
  under </span><span lang=EN-GB style='font-family:Symbol;mso-ansi-language:
  EN-GB'>b</span><span lang=EN-GB style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-ansi-language:EN-GB'> is derived
  from its predecessor by an A-operation.<span style="mso-spacerun: yes">&nbsp;
  </span>In the case of (b), the inverse of L<sub>n+1</sub> under </span><span
  lang=EN-GB style='font-family:Symbol;mso-ansi-language:EN-GB'>b</span><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'> is derived from its predecessor
  by a B-operation. <u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>We will call the operation on L<sub>n</sub>
  that corresponds to case (a) <b>the</b> <b>A<sub>n</sub> operation</b>, and
  an operation that corresponds to case (b) is <b>a B<sub>n</sub> operation</b>.
  ABn series are thus built up from a list containing a single number, by
  successively iterating A<sub>n</sub> and B<sub>n</sub> operations. Since the
  elements of an AB series are correlated 1-1 with elements of the
  corresponding ABn series, we can show that there is no infinite AB series by
  proving the following theorem.<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><b><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>Theorem:</span></b><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'> There is no infinite ABn series.<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoBodyText style='margin-left:.5in'><span lang=EN-GB
  style='font-size:10.0pt;font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'>Let us say that an ABn series is <b>protracted</b>, if
  there is no element L in the series that lacks a successor when an An or Bn
  operation could be successfully applied to L.<span style="mso-spacerun:
  yes">&nbsp; </span>We shall prove that there is no infinite ABn series by
  proving the following result.<span style="mso-spacerun: yes">&nbsp; </span><span
  style="mso-spacerun: yes">&nbsp;</span><u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><b><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>Theorem:</span></b><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'><span style="mso-spacerun:
  yes">&nbsp; </span>If L<sub>n</sub> is a non-empty list of numbers in a
  protracted ABn series, then tail(L<sub>n</sub>) occurs in the series.<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><b><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>Proof:</span></b><span lang=EN-GB
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman";
  mso-ansi-language:EN-GB'><span style="mso-spacerun: yes">&nbsp; </span>the
  proof proceeds by use of strong induction over the value of the first number <i>a</i>
  in L<sub>n</sub>.<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><b><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>Base Case:</span></b><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'> <i>a</i> = 0.<span
  style="mso-spacerun: yes">&nbsp;&nbsp; </span>Then the only admissible ABn
  operation that can be carried out on L<sub>n</sub> is the An operation, and
  so L<sub>n+1</sub> = tail(L<sub>n</sub>) and the theorem is proved.<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><b><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>Inductive Case:</span></b><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'><span style="mso-spacerun:
  yes">&nbsp; </span>the theorem holds for all values for <i>a</i> of less than
  <i>m</i>. Let L<sub>n</sub> = [<i>m</i>,&#8230;.]. Consider L<sub>n+1</sub>.<span
  style="mso-spacerun: yes">&nbsp; </span>Either<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify;text-indent:
  -.25in;mso-list:l0 level1 lfo6;tab-stops:list .5in'><![if !supportLists]>(a)<span
  style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp; </span><![endif]><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>(a)</span><span lang=EN-GB
  style='font-size:7.0pt;mso-ansi-language:EN-GB'>&nbsp;&nbsp;&nbsp; </span><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>L<sub>n+1</sub> is derived from L<sub>n</sub>
  by the A<sub>n</sub> operation.<span style="mso-spacerun: yes">&nbsp;
  </span>If so, L<sub>n+1</sub> = tail(L<sub>n</sub>) and the theorem is proved.<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify;text-indent:
  -.25in;mso-list:l0 level1 lfo6;tab-stops:list .5in'><![if !supportLists]>(b)<span
  style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp; </span><![endif]><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>(b)</span><span lang=EN-GB
  style='font-size:7.0pt;mso-ansi-language:EN-GB'>&nbsp;&nbsp;&nbsp; </span><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>L<sub>n+1</sub> is derived from L<sub>n</sub>
  by a B<sub>n</sub> operation.<span style="mso-spacerun: yes">&nbsp; </span>In
  which case L<sub>n+1</sub> = [<i>b</i><sub>1</sub>,&#8230;,<i>b</i><sub>k </sub>|
  tail(L<sub>n</sub>)].<span style="mso-spacerun: yes">&nbsp; </span>Since each
  of the <i>b</i><sub>1</sub>,&#8230;,<i>b</i><sub>k </sub>is less than <i>m</i>, the
  inductive hypothesis applies to each of [<i>b</i><sub>1</sub>,&#8230;,<i>b</i><sub>k
  </sub>| tail(L<sub>n</sub>)], [<i>b</i><sub>2</sub>,&#8230;,<i>b</i><sub>k </sub>|
  tail(L<sub>n</sub>)] &#8230;.. and so on to [<i>b</i><sub>k </sub>| tail(L<sub>n</sub>)].<span
  style="mso-spacerun: yes">&nbsp; </span>But if the inductive hypothesis
  applies to<span style="mso-spacerun: yes">&nbsp; </span>[<i>b</i><sub>k </sub>|
  tail(L<sub>n</sub>)], then tail(L<sub>n</sub>) occurs in the series and the
  theorem is proved.<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><b><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>Theorem:</span></b><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'> every protracted ABn series is
  terminated by the empty list.<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><b><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>&nbsp;<u3:p></u3:p></span></b></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><b><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>Proof:</span></b><span lang=EN-GB
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman";
  mso-ansi-language:EN-GB'> every ABn series begins with a list containing a
  single number and the tail of that list is the empty list.<span
  style="mso-spacerun: yes">&nbsp; </span>Since no ABn operation can be applied
  to the empty list, any protracted ABn series terminates with the empty list.<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><b><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>&nbsp;<u3:p></u3:p></span></b></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><b><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>Theorem:</span></b><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'> there is no infinite ABn series.<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><b><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>Proof:</span></b><span lang=EN-GB
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman";
  mso-ansi-language:EN-GB'> assume X is an infinite ABn series.<span
  style="mso-spacerun: yes">&nbsp; </span>Every infinite ABn series must be
  protracted, since if it were not, it would terminate with a list to which an
  ABn operation could be applied.<span style="mso-spacerun: yes">&nbsp;
  </span>So X is protracted and since every protracted ABn series terminates
  with [ ], X is a terminating infinite series.<span style="mso-spacerun:
  yes">&nbsp;&nbsp; </span>By <i>reductio</i>, X does not exist.<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>Hence we can finally assert.<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><b><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>The AB Theorem:</span></b><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'> there is no infinite AB series.<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoBodyText style='margin-left:.5in'><b><span lang=EN-GB
  style='font-size:10.0pt;font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'>Proof:</span></b><span lang=EN-GB style='font-size:10.0pt;
  font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style="mso-spacerun: yes">&nbsp; </span>since the elements of every AB series
  are correlated 1-1 with every ABn series, since there is no infinite ABn
  series, there is no infinite AB series.<u3:p></u3:p></span></p>
  <p class=MsoBodyText style='margin-left:.5in'><span lang=EN-GB
  style='font-size:10.0pt;font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><b><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>Theorem:</span></b><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'> </span><span lang=EN-GB
  style='font-family:BrushScrD;mso-ansi-language:EN-GB;mso-bidi-font-style:
  italic'>T </span><span lang=EN-GB style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-ansi-language:EN-GB;mso-bidi-font-weight:
  bold'>is terminating.<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoBodyText style='margin-left:.5in'><b><span lang=EN-GB
  style='font-size:10.0pt;font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'>Proof:</span></b><span lang=EN-GB style='font-size:10.0pt;
  font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>
  If </span><span lang=EN-GB style='font-family:BrushScrD;mso-bidi-font-style:
  italic'>T</span><span lang=EN-GB style='font-size:10.0pt;font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'> <span style='mso-bidi-font-weight:
  bold'>failed to terminate, then there would be an infinitely long AB series</span>.<u3:p></u3:p></span></p>
  <p class=MsoBodyText style='margin-left:.5in'><b><u><span lang=EN-GB
  style='font-size:14.0pt;mso-bidi-font-size:10.0pt;font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>&nbsp;<u3:p></u3:p></span></u></b></p>
  <p class=MsoBodyText style='margin-left:.5in'><b><u><span lang=EN-GB
  style='font-size:14.0pt;mso-bidi-font-size:10.0pt;font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>Unification and the AB
  Theorem_____________<u3:p></u3:p></span></u></b></p>
  <p class=MsoBodyText style='margin-left:.5in'><span lang=EN-GB
  style='font-size:10.0pt;font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoBodyText style='margin-left:.5in'><span lang=EN-GB
  style='font-size:10.0pt;font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-bidi-font-weight:bold'>The AB theorem</span><!--[if supportFields]><span
  lang=EN-GB style='font-size:10.0pt;font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-bidi-font-weight:bold'><span
  style='mso-element:field-begin'></span></span><span lang=EN-GB
  style='font-size:10.0pt;font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'> XE &quot;<span style='mso-bidi-font-weight:bold'>AB
  theorem</span>&quot; </span><![endif]--><!--[if supportFields]><span
  lang=EN-GB style='font-size:10.0pt;font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-bidi-font-weight:bold'><span
  style='mso-element:field-end'></span></span><![endif]--><span lang=EN-GB
  style='font-size:10.0pt;font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-bidi-font-weight:bold'><span style="mso-spacerun:
  yes">&nbsp;</span>seems to contradict with an example of non-termination that
  was raised at the end of chapter 13.<span style="mso-spacerun: yes">&nbsp;
  </span>We saw that an attempt to define the type operator <b>or</b> lead to
  an infinite regress &#8211; precisely the case that the AB theorem was designed to
  block.<span style="mso-spacerun: yes">&nbsp; </span>The rule that lead to
  this regress was<u3:p></u3:p></span></p>
  <p class=MsoBodyText style='margin-left:.5in'><b><u><span lang=EN-GB
  style='font-size:10.0pt;font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'>&nbsp;<u3:p></u3:p></span></u></b></p>
  <p class=MsoBodyText style='margin-left:.5in'><b><u><span lang=EN-GB
  style='font-size:10.0pt;font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'>X : A;<u3:p></u3:p></span></u></b></p>
  <p class=MsoBodyText style='margin-left:.5in'><b><span lang=EN-GB
  style='font-size:10.0pt;font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'>X : (A or B);<u3:p></u3:p></span></b></p>
  <p class=MsoBodyText style='margin-left:.5in'><span lang=EN-GB
  style='font-size:10.0pt;font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-bidi-font-weight:bold'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoBodyText style='margin-left:.5in'><span lang=EN-GB
  style='font-size:10.0pt;font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-bidi-font-weight:bold'>Inspection shows this rule to
  behave like a B-rule. How, in the light of our reasoning so far, can this
  rule lead to an infinite regress?<u3:p></u3:p></span></p>
  <p class=MsoBodyText style='margin-left:.5in'><span lang=EN-GB
  style='font-size:10.0pt;font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-bidi-font-weight:bold'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoBodyText style='margin-left:.5in'><span lang=EN-GB
  style='font-size:10.0pt;font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-bidi-font-weight:bold'>The culprit is of course,
  unification.<span style="mso-spacerun: yes">&nbsp; </span>The AB theorem</span><!--[if supportFields]><span
  lang=EN-GB style='font-size:10.0pt;font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-bidi-font-weight:bold'><span
  style='mso-element:field-begin'></span></span><span lang=EN-GB
  style='font-size:10.0pt;font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'> XE &quot;<span style='mso-bidi-font-weight:bold'>AB
  theorem</span>&quot; </span><![endif]--><!--[if supportFields]><span
  lang=EN-GB style='font-size:10.0pt;font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-bidi-font-weight:bold'><span
  style='mso-element:field-end'></span></span><![endif]--><span lang=EN-GB
  style='font-size:10.0pt;font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-bidi-font-weight:bold'><span style="mso-spacerun:
  yes">&nbsp;</span>assumes that all AB rules are interpreted conventionally
  through pattern-matching.<span style="mso-spacerun: yes">&nbsp;
  </span>However, even an innocuous B rule can become expansive if filtered
  through unification.<span style="mso-spacerun: yes">&nbsp; </span>The </span><span
  lang=EN-GB style='font-family:BrushScrD;mso-bidi-font-style:italic'>T</span><span
  lang=EN-GB style='font-size:10.0pt;font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-bidi-font-weight:bold'> algorithm
  secures termination via the AB theorem because it dispenses with the non-B <i>Specialisation
  Rule.<span style="mso-spacerun: yes">&nbsp; </span></i>But unification brings
  its own dangers, so it remains to be shown that this sort of non-terminating
  case does not arise.<u3:p></u3:p></span></p>
  <p class=MsoBodyText style='margin-left:.5in'><span lang=EN-GB
  style='font-size:10.0pt;font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-bidi-font-weight:bold'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoBodyText style='margin-left:.5in'><span lang=EN-GB
  style='font-size:10.0pt;font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-bidi-font-weight:bold'>Fortunately this is not too
  hard.<span style="mso-spacerun: yes">&nbsp; </span></span><span lang=EN-GB
  style='font-family:BrushScrD;mso-bidi-font-style:italic'>T</span><span
  lang=EN-GB style='font-size:10.0pt;font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-bidi-font-weight:bold'> applies <i>unification</i>
  with respect to <i>types</i> and <i>pattern-matching</i> with respect to </span><span
  lang=EN-GB style='font-family:BrushScrD;mso-bidi-font-style:italic'>L</span><span
  lang=EN-GB style='font-size:10.0pt;font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-bidi-font-weight:bold'>
  expressions.<span style="mso-spacerun: yes">&nbsp; </span>To verify that the
  AB theorem</span><!--[if supportFields]><span lang=EN-GB style='font-size:
  10.0pt;font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman";
  mso-bidi-font-weight:bold'><span style='mso-element:field-begin'></span></span><span
  lang=EN-GB style='font-size:10.0pt;font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'> XE &quot;<span style='mso-bidi-font-weight:
  bold'>AB theorem</span>&quot; </span><![endif]--><!--[if supportFields]><span
  lang=EN-GB style='font-size:10.0pt;font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-bidi-font-weight:bold'><span
  style='mso-element:field-end'></span></span><![endif]--><span lang=EN-GB
  style='font-size:10.0pt;font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-bidi-font-weight:bold'><span style="mso-spacerun:
  yes">&nbsp;</span>still applies, we need only show that, after any type rule
  is applied, the B-value decreases through a reduction in the B-value of the</span><span
  lang=EN-GB style='font-family:BrushScrD;mso-bidi-font-style:italic'> L</span><span
  lang=EN-GB style='font-size:10.0pt;font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-bidi-font-weight:bold'> expression
  and not because of a reduction in the B-value of the type.<span
  style="mso-spacerun: yes">&nbsp;&nbsp; </span>Inspection shows this to be
  true of every rule in the system bar one &#8211; the <i>Generalisation Rule</i>.<span
  style="mso-spacerun: yes">&nbsp; </span>Allowing this rule requires us to
  make some caveats.<u3:p></u3:p></span></p>
  <p class=MsoBodyText style='margin-left:.5in'><span lang=EN-GB
  style='font-size:10.0pt;font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-bidi-font-weight:bold'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoBodyText style='margin-left:.5in'><span lang=EN-GB
  style='font-size:10.0pt;font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'>Using backward chaining, the <i>Generalisation Rule</i>
  eliminates the universal quantifiers at the front of type expressions.<span
  style="mso-spacerun: yes">&nbsp; </span>The only place where this rule is
  invoked is in the proof of the type-security of polymorphic functions.<span
  style="mso-spacerun: yes">&nbsp; </span>Moreover since <span
  style='mso-bidi-font-style:italic'>Qi</span> is an <b>explicitly typed</b></span><!--[if supportFields]><b><span
  lang=EN-GB style='font-size:10.0pt;font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'><span style='mso-element:field-begin'></span></span></b><span
  lang=EN-GB style='font-size:10.0pt;font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'> XE &quot;<b>explicitly typed</b>&quot;
  </span><![endif]--><!--[if supportFields]><b><span lang=EN-GB
  style='font-size:10.0pt;font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'><span style='mso-element:field-end'></span></span></b><![endif]--><b><span
  lang=EN-GB style='font-size:10.0pt;font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'><span style="mso-spacerun:
  yes">&nbsp;</span>language</span></b><a style='mso-footnote-id:ftn1'
  href="#_ftn1" name="_ftnref1" title=""><span class=MsoFootnoteReference><span
  lang=EN-GB style='font-size:10.0pt;font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'><span style='mso-special-character:
  footnote'><![if !supportFootnotes]>[1]<![endif]></span></span></span></a><span
  class=MsoFootnoteReference><span lang=EN-GB style='font-size:10.0pt;
  font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>[1]</span></span><b><span
  lang=EN-GB style='font-size:10.0pt;font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'> </span></b><span lang=EN-GB
  style='font-size:10.0pt;font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'>where all types are shallow, if we allow this rule to be
  interpreted <i>modulo</i> pattern-matching, without unification, just at the
  beginning of the proof, then with this caveat, the AB theorem</span><!--[if supportFields]><span
  lang=EN-GB style='font-size:10.0pt;font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'><span style='mso-element:field-begin'></span>
  XE &quot;<span style='mso-bidi-font-weight:bold'>AB theorem</span>&quot; </span><![endif]--><!--[if supportFields]><span
  lang=EN-GB style='font-size:10.0pt;font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'><span style='mso-element:field-end'></span></span><![endif]--><span
  lang=EN-GB style='font-size:10.0pt;font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'><span style="mso-spacerun:
  yes">&nbsp;</span>still applies.<span style="mso-spacerun: yes">&nbsp;
  </span>Alternatively, we may follow </span><span lang=EN-GB style='font-family:
  BrushScrD;mso-bidi-font-style:italic'>T</span><span lang=EN-GB
  style='font-size:10.0pt;font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'>* and simply eliminate such universally bound variables by
  fresh terms &#8211; eliminating any need for the <i>Generalisation Rule </i>at all.<u3:p></u3:p></span></p>
  <p class=MsoBodyText style='margin-left:.5in'><b><span lang=EN-GB
  style='font-size:10.0pt;font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'>&nbsp;<u3:p></u3:p></span></b></p>
  <p class=MsoBodyText style='margin-left:.5in'><b><u><span lang=EN-GB
  style='font-size:14.0pt;mso-bidi-font-size:10.0pt;font-family:BrushScrD;
  mso-bidi-font-style:italic'>T</span></u></b><b><u><span lang=EN-GB
  style='font-size:14.0pt;mso-bidi-font-size:10.0pt;font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'> and
  Completeness________________________<u3:p></u3:p></span></u></b></p>
  <p class=MsoBodyText style='margin-left:.5in'><b><span lang=EN-GB
  style='font-size:10.0pt;font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'>&nbsp;<u3:p></u3:p></span></b></p>
  <p class=MsoBodyText style='margin-left:.5in'><span lang=EN-GB
  style='font-family:BrushScrD;mso-bidi-font-style:italic'>T</span><span
  lang=EN-GB style='font-size:10.0pt;font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'> is not complete with respect to the
  type system of </span><span lang=EN-GB style='font-family:BrushScrD;
  mso-bidi-font-style:italic'>L</span><span lang=EN-GB style='font-size:10.0pt;
  font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>.<span
  style="mso-spacerun: yes">&nbsp; </span>Functions that involve <b>generic
  type variables</b></span><!--[if supportFields]><b><span lang=EN-GB
  style='font-size:10.0pt;font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'><span style='mso-element:field-begin'></span></span></b><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'> XE &quot;</span><b><span lang=EN-GB style='font-size:
  10.0pt;font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>generic</span></b><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'>&quot; </span><![endif]--><!--[if supportFields]><b><span
  lang=EN-GB style='font-size:10.0pt;font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'><span style='mso-element:field-end'></span></span></b><![endif]--><a
  style='mso-footnote-id:ftn2' href="#_ftn2" name="_ftnref2" title=""><span
  class=MsoFootnoteReference><span lang=EN-GB style='font-size:10.0pt;
  font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style='mso-special-character:footnote'><![if !supportFootnotes]>[2]<![endif]></span></span></span></a><span
  class=MsoFootnoteReference><span lang=EN-GB style='font-size:10.0pt;
  font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>[2]</span></span><span
  lang=EN-GB style='font-size:10.0pt;font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'> will not be type-checked by </span><span
  lang=EN-GB style='font-family:BrushScrD;mso-bidi-font-style:italic'>T</span><span
  lang=EN-GB style='font-size:10.0pt;font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>.<span style="mso-spacerun:
  yes">&nbsp; </span>The following example is adapted from Field and Harrison
  (1988).<u3:p></u3:p></span></p>
  <p class=MsoBodyText style='margin-left:.5in'><span lang=EN-GB
  style='font-size:10.0pt;font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoBodyText style='margin-left:.5in'><b><span lang=EN-GB
  style='font-size:10.0pt;font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Courier New"'>(define f<u3:p></u3:p></span></b></p>
  <p class=MsoBodyText style='margin-left:.5in'><b><span lang=EN-GB
  style='font-size:10.0pt;font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Courier New"'><span style="mso-spacerun: yes">&nbsp; </span>{A - -&gt;
  (number * boolean)}<u3:p></u3:p></span></b></p>
  <p class=MsoBodyText style='margin-left:.5in'><b><span lang=EN-GB
  style='font-size:10.0pt;font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Courier New"'><span style="mso-spacerun: yes">&nbsp;&nbsp; </span>X -&gt;
  (let F (/. Y Y) (@p (F 3) (F true)))<u3:p></u3:p></span></b></p>
  <p class=MsoBodyText style='margin-left:.5in'><span lang=EN-GB
  style='font-size:10.0pt;font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoBodyText style='margin-left:.5in'><span lang=EN-GB
  style='font-size:10.0pt;font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'>The function does have the type A </span><span lang=EN-GB
  style='font-size:10.0pt;mso-bidi-font-size:12.0pt;font-family:Symbol'>�</span><span
  lang=EN-GB style='font-size:10.0pt;font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'> (number * boolean) in our type
  system.<span style="mso-spacerun: yes">&nbsp; </span>However </span><span
  lang=EN-GB style='font-family:BrushScrD;mso-bidi-font-style:italic'>T </span><span
  lang=EN-GB style='font-size:10.0pt;font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>will not recognise it as well typed,
  generating the problems.<u3:p></u3:p></span></p>
  <p class=MsoBodyText style='margin-left:.5in'><span lang=EN-GB
  style='font-size:10.0pt;font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoBodyText style='margin-left:.5in'><b><span lang=EN-GB
  style='font-size:10.0pt;font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Courier New"'>x : a &gt;&gt; (/. Y Y) : B <u3:p></u3:p></span></b></p>
  <p class=MsoBodyText style='margin-left:.5in'><b><span lang=EN-GB
  style='font-size:10.0pt;font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Courier New";letter-spacing:-.2pt'>x : a, (/. Y Y) : B &gt;&gt; (@p (F 3) (F
  true)) : (number * boolean)<u3:p></u3:p></span></b></p>
  <p class=MsoBodyText style='margin-left:.5in'><span lang=EN-GB
  style='font-family:BrushScrD;mso-bidi-font-style:italic'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoBodyText style='margin-left:.5in'><span lang=EN-GB
  style='font-size:10.0pt;font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";letter-spacing:-.1pt'>Application of the <i>Generalisation
  Rule</i> <i>modulo</i> unification will solve the first problem, but then B
  has to be instantiated in two different ways, so this function will not be
  type-checked in <span style='mso-bidi-font-style:italic'>Qi</span>. <u3:p></u3:p></span></p>
  <p class=MsoBodyText style='margin-left:.5in'><span lang=EN-GB
  style='font-size:10.0pt;font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoFootnoteText style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-size:10.0pt;font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-ansi-language:EN-GB'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal>&nbsp;<u3:p></u3:p></p>
  <p><br clear=all style='mso-special-character:line-break'>
  </p>
  <div class=MsoNormal><span style='font-size:12.0pt'>
  <hr size=1 width="33%" align=left>
  </span></div>
  <p class=MsoFootnoteText style='text-align:justify'><a style='mso-footnote-id:
  ftn3' href="#_ftn3" name="_ftnref3" title=""><span
  class=MsoFootnoteReference><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'><span style='mso-special-character:
  footnote'><![if !supportFootnotes]>[3]<![endif]></span></span></span></a><span
  class=MsoFootnoteReference><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>[1]</span></span><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>
  </span><span style='font-size:8.0pt;mso-bidi-font-size:10.0pt;font-family:
  "Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>That is, the type
  the function is supposed to have must be explicitly given in the function
  itself.<span style="mso-spacerun: yes">&nbsp; </span>Other functional
  languages (like SML for instance) are <b>implicitly typed</b></span><!--[if supportFields]><b><span
  style='font-size:8.0pt;mso-bidi-font-size:10.0pt;font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'><span style='mso-element:field-begin'></span></span></b><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>
  XE &quot;</span><b><span style='font-size:8.0pt;mso-bidi-font-size:10.0pt;
  font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>implicitly
  typed</span></b><span style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'>&quot; </span><![endif]--><!--[if supportFields]><b><span
  style='font-size:8.0pt;mso-bidi-font-size:10.0pt;font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'><span style='mso-element:field-end'></span></span></b><![endif]--><span
  style='font-size:8.0pt;mso-bidi-font-size:10.0pt;font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>.<span style="mso-spacerun:
  yes">&nbsp; </span>This means that the language does not require the user to state
  the type, but instead tries to infer it.<u3:p></u3:p></span></p>
  <p class=MsoFootnoteText><a style='mso-footnote-id:ftn4' href="#_ftn4"
  name="_ftnref4" title=""><span class=MsoFootnoteReference><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style='mso-special-character:footnote'><![if !supportFootnotes]>[4]<![endif]></span></span></span></a><span
  class=MsoFootnoteReference><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>[2]</span></span><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>
  </span><span style='font-size:8.0pt;mso-bidi-font-size:10.0pt;font-family:
  "Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>See Field and
  Harrison (1988) (p 148-149) for a discussion of generic</span><!--[if supportFields]><span
  style='font-size:8.0pt;mso-bidi-font-size:10.0pt;font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'><span style='mso-element:field-begin'></span></span><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>
  XE &quot;</span><b><span style='font-size:10.0pt;font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>generic</span></b><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>&quot;
  </span><![endif]--><!--[if supportFields]><span style='font-size:8.0pt;
  mso-bidi-font-size:10.0pt;font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'><span style='mso-element:field-end'></span></span><![endif]--><span
  style='font-size:8.0pt;mso-bidi-font-size:10.0pt;font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'><span style="mso-spacerun:
  yes">&nbsp;</span>types.<u3:p></u3:p></span></p>
  </td>
 </tr>
</table>

</div>

<p class=MsoNormal><span style='font-size:12.0pt'><![if !supportEmptyParas]>&nbsp;<![endif]><o:p></o:p></span></p>

</div>

<div style='mso-element:footnote-list'><![if !supportFootnotes]><br clear=all>

<hr align=left size=1 width="33%">

<![endif]>

<div style='mso-element:footnote' id=ftn1>

<p class=MsoNormal><a style='mso-footnote-id:ftn1' href="#_ftnref1" name="_ftn1"
title=""></a><![if !supportEmptyParas]>&nbsp;<![endif]><o:p></o:p></p>

</div>

<div style='mso-element:footnote' id=ftn2>

<p class=MsoNormal><a style='mso-footnote-id:ftn2' href="#_ftnref2" name="_ftn2"
title=""></a><![if !supportEmptyParas]>&nbsp;<![endif]><o:p></o:p></p>

</div>

<div style='mso-element:footnote' id=ftn3>

<p class=MsoNormal><a style='mso-footnote-id:ftn3' href="#_ftnref3" name="_ftn3"
title=""></a><![if !supportEmptyParas]>&nbsp;<![endif]><o:p></o:p></p>

</div>

<div style='mso-element:footnote' id=ftn4>

<p class=MsoNormal><a style='mso-footnote-id:ftn4' href="#_ftnref4" name="_ftn4"
title=""></a><![if !supportEmptyParas]>&nbsp;<![endif]><o:p></o:p></p>

</div>

</div>

</body>

</html>
